\chapter*{Abstract}
\thispagestyle{empty}

Nowadays, programming languages have keep to up with new requirements determined by hardware evolution and software development. As a consequence, programming languages are becoming more and more complex; therefore we need precise specifications for them. An executable formal specification is one of the most effective ways to define programming languages because it can both execute and formally reason about programs. \K is a rewriting based framework which can be used for defining, testing, and analyzing such formal specifications making use of configurations, computations and rules.

A \K definition for a programming language is compiled into a rewrite theory by applying some transformations steps. The aim of this dissertation is to analyze the contextual transformation. To improve the modularity of definitions, a \K rule only specifies the {\em minimal required} context for its application. The contextual transformation step uses the static information about the structure of the global running configuration to infer {\em sufficiently}  additional context to make the rule match and apply on the running configuration. Complex definitions, like the K definition of C language, for example, prove that sometimes the existing implementation leads to unexpected behaviors. 

Some limitations of the existing approach are that (1) the configuration cannot contain cells with the same name, (2) the cases where the context transformations could have more than one solution are not analyzed, and (3) the locality principle does not have yet an unanimously agreed formal specification. In this dissertation, an investigation of all these limitations is done in order to find correct formal definitions which can then be combined to obtain a well-defined contextual transformation algorithm. 

The {\bf main contributions of the dissertation} are the following: (1) complete description of the contextual transformation,  (2) several algorithms for finding all possible contexts for a given rule, (3) a formal definition for the locality principle, (4) several consistency checks and filtering contexts, (5) an algorithm for finding the final unambiguous context of a rule.
